FDL - Step of Proof: fun_exp_add-sq

Step of Proof: fun_exp_add-sq

Inference at *
Iof proof for Lemma fun exp add-sq:

n, m:

, f, x:Top. (f^n+m(x)) ~ (f^n(f^m(x)))

by ((Unfold `fun_exp` ( 0)

)

CollapseTHEN (((InductionOnNat)

CollapseTHEN (((Reduce 0)

CoCollapseTHEN (((((UnivCD)

CollapseTHENA (Auto

))

)

CollapseTHEN ((Try ((Complete (Auto

))

))

C))

))

))

))

C1:

C1: 1. n :

C1: 2. 0 < n

C1: 3.

m:

, f, x:Top.

C1: 3. (primrec((n - 1)+m;

x.x;

i,g. f o g)(x))

C1: 3. ~

C1: 3. (primrec(n - 1;

x.x;

i,g. f o g)(primrec(m;

x.x;

i,g. f o g)(x)))

C1: 4. m :

C1: 5. f : Top

C1: 6. x : Top

C1:

(primrec(n+m;

x.x;

i,g. f o g)(x))

C1:

~

C1:

(primrec(n;

x.x;

i,g. f o g)(primrec(m;

x.x;

i,g. f o g)(x)))

C.

Definitions Void, -n, i j , f^n, S T, |g|, n+m, n - m, #$n, SQType(T), {x:A| B(x)} , A B, A, False, P Q, s ~ t, {T}, Type, f(a), primrec(n;b;c), x.A(x), f o g, , x:A. B(x), x:AB(x), a < b, , Top, , s = t, t T

Lemmas ge wf, nat properties, nat ind tp, nat wf, guard wf, top wf